package org.goobs.logic;

import java.util.Collection;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.StringTokenizer;

public class WellFormedFormula {

	protected static final int ATOMIC = 0;
	protected static final int NEGATION = 1;
	protected static final int CONJUNCTION = 2;
	protected static final int QUANTIFIER = 3;

	private int type;

	//--Atomic
	private String predName;
	private List<String> predArgs;
	//--Symbolic
	private Symbol symb;
	private List<WellFormedFormula> args;
	//(negation)
	//(conjunction)
	//(quantifier)
	private String quantVar;

	private List<Object> scm = new LinkedList<Object>();

	private WellFormedFormula() {
	}

	public WellFormedFormula(String expr, Collection<Symbol> validSymbols) {
		parse(expr);
		generateSemantics(validSymbols);

	}

	@SuppressWarnings("unchecked")
	private void parse(String expr) {
		StringTokenizer tokens = new StringTokenizer("( "
				+ cleanSchemeSyntax(expr) + " )");
		scm = parse(tokens);
		if (scm.size() != 1 || !(scm.get(0) instanceof List)) {
			throw new IllegalArgumentException("Internal error parsing: "
					+ expr);
		}
		scm = (List<Object>) scm.get(0);
	}

	private List<Object> parse(StringTokenizer tokens) {
		LinkedList<Object> rtn = new LinkedList<Object>();
		String token;
		while (tokens.hasMoreTokens()
				&& !(token = tokens.nextToken()).equals(")")) {
			Object toAdd = null;
			if (token.equals("(")) {
				toAdd = parse(tokens);
			} else {
				toAdd = token;
			}
			rtn.add(toAdd);
		}
		return rtn;
	}

	private static String cleanSchemeSyntax(String str) {
		str = str.toLowerCase();
		String rtn = "";

		//more complex expressions
		int paren = 0;
		for (int i = 0; i < str.length(); i++) {
			if (str.charAt(i) == '(') {
				paren++;
				rtn = rtn + " ( ";
			} else if (str.charAt(i) == ')') {
				paren--;
				rtn = rtn + " ) ";
			} else if (str.charAt(i) == '"') {
				rtn = rtn + "\" ";
				i++;
				while (str.charAt(i) != '"') {
					if (i == str.length() - 1) {
						throw new IllegalArgumentException(
								"quotes do not match: " + str);
					}
					rtn = rtn + str.charAt(i);
					i++;
				}
				rtn = rtn + " \" ";
			} else if (str.charAt(i) == ';') {
				while (i < str.length() && str.charAt(i) != '\n') {
					i++;
				}
				rtn = rtn + " ";
			} else {
				rtn = rtn + str.charAt(i);
			}
		}
		if (paren != 0) {
			throw new IllegalArgumentException("parenthesis do not match: "
					+ rtn);
		}
		return rtn;
	}

	public void printTree() {
		System.out.println("Expression: ");
		printTreeHelper(scm, "");
	}

	@SuppressWarnings("unchecked")
	private void printTreeHelper(List<Object> lst, String prefix) {
		for (Object o : lst) {
			if (o instanceof List) {
				printTreeHelper((List<Object>) o, prefix + "   ");
			} else {
				System.out.println(prefix + o);
			}
		}
	}

	@SuppressWarnings("unchecked")
	private void generateSemantics(Collection<Symbol> validSymbols) {
		if (scm.size() > 1) {
			throw new IllegalArgumentException(
					"Cannot parse multiple expressions in one line");
		}
		if (!(scm.get(0) instanceof List)) {
			throw new IllegalArgumentException("Not a well formed formula: "
					+ scm.get(0));
		}
		generateSemantics((List) scm.get(0), validSymbols);
	}

	private void generateSemantics(List<Object> lst,
			Collection<Symbol> validSymbols) {
		Iterator<Object> iter = lst.iterator();
		Object tp = iter.next();
		Symbol symb = Symbol.parse(tp.toString());
		if (validSymbols.contains(symb)) {
			//--Case symbol
			generateSymb(symb, iter, validSymbols);
		} else {
			//--Case predicate
			this.type = ATOMIC;
			predName = tp.toString();
			predArgs = new LinkedList<String>();
			while (iter.hasNext()) {
				Object term = iter.next();
				if (!(term instanceof String)) {
					throw new IllegalArgumentException(
							"Encountered non-string argument for predicate: "
									+ predName + " term: " + term);
				}
				predArgs.add(term.toString());
			}
		}
	}

	private void generateSymb(Symbol symb, Iterator<Object> iter,
			Collection<Symbol> validSymbols) {
		this.symb = symb;

		switch (symb) {

		//--EQUALS
		case EQUALS:
			this.type = ATOMIC;
			predArgs = new LinkedList<String>();
			try {
				predArgs.add((String) iter.next());
				predArgs.add((String) iter.next());
			} catch (RuntimeException e) {
				throw new IllegalArgumentException(
						"Equals has less than two terms, or some non-String terms");
			}
			if (iter.hasNext()) {
				throw new IllegalArgumentException(
						"Equals has more than two terms");
			}
			break;

		//--NOT
		case NOT:
			this.type = NEGATION;
			args = buildArgs(iter, validSymbols, 1, 1);
			break;

		//--AND/OR
		case AND:
		case OR:
			this.type = CONJUNCTION;
			args = buildArgs(iter, validSymbols, 2, Integer.MAX_VALUE);
			break;

		//--COND
		case BICOND:
		case COND:
			this.type = CONJUNCTION;
			args = buildArgs(iter, validSymbols, 2, 2);
			break;

		case EXISTS:
		case FORALL:
			this.type = QUANTIFIER;
			Object var = iter.next();
			if (!(var instanceof String)) {
				throw new IllegalArgumentException(
						"quantifier variable should be a string: " + var);
			}
			this.quantVar = (String) var;
			args = buildArgs(iter, validSymbols, 1, 1);
			break;

		default:
			throw new IllegalArgumentException("Unknown symbol type: " + symb);

		}
	}

	@SuppressWarnings("unchecked")
	private List<WellFormedFormula> buildArgs(Iterator<Object> iter,
			Collection<Symbol> validSymbols, int minLength, int maxLength) {
		List<WellFormedFormula> rtn = new LinkedList<WellFormedFormula>();
		while (iter.hasNext()) {
			Object term = iter.next();
			if (term instanceof List) {
				WellFormedFormula dummy = new WellFormedFormula();
				dummy.generateSemantics((List) term, validSymbols);
				rtn.add(dummy);
			} else {
				throw new IllegalArgumentException("Arguments to " + symb
						+ " should be well formed formulas");

			}
		}
		if (rtn.size() < minLength || rtn.size() > maxLength) {
			throw new IllegalArgumentException("bad number of arguments to "
					+ this.symb + " actual: " + rtn.size()
					+ " should be between [" + minLength + ", " + maxLength
					+ "]");
		}
		return rtn;
	}
	
	
	protected int getType(){
		return type;
	}
	protected String getName(){
		return predName;
	}
	protected List <String> predArgs(){
		return predArgs;
	}
	protected Symbol getSymbol(){
		return symb;
	}
	protected List <WellFormedFormula> getArgs(){
		return args;
	}
	protected String getQuantVar(){
		return quantVar;
	}
	

	public String toString() {
		String con = null;
		String rtn;
		if (this.type == ATOMIC) {
			if (this.predName == null) {
				//--Case equals
				return this.predArgs.get(0) + "=" + this.predArgs.get(1);
			} else {
				//--Case predicate
				rtn = this.predName + "(";
				for (String term : this.predArgs) {
					rtn = rtn + term + ", ";
				}
				rtn = rtn.substring(0, rtn.length() - 2) + ")";
				return rtn;
			}
		} else {
			switch (this.symb) {
			case AND:
				con = " ^ ";
			case OR:
				if (con == null) {
					con = " v ";
				}
			case COND:
				if (con == null) {
					con = " --> ";
				}
			case BICOND:
				if (con == null) {
					con = " <-> ";
				}

				rtn = "";
				for (WellFormedFormula x : args) {
					rtn = rtn + x + con;
				}
				rtn = rtn.substring(0, rtn.length() - 3);
				return rtn;

			case NOT:
				return "~" + args.get(0);

			case FORALL:
				rtn = "ALL{" + quantVar + "}[ " + args.get(0) + " ]";
				return rtn;
			case EXISTS:
				rtn = "EXIST{" + quantVar + "}[ " + args.get(0) + " ]";
				return rtn;

			default:
				return "UNKNOWN QUANTIFIER: " + symb;
			}
		}
	}

}
